Seminar: Formale Methoden der Hardware-Verifikation

Beschreibung:
Hardware-Verifikation ist der Versuch, mit Hilfe formaler Methoden die Korrektheit von Schaltkreisen nachzuweisen. In diesem Seminar sollen die Teilnehmer sowohl die Methoden, als auch die daraus entwickelten Werkzeuge kennenlernen. Die Themengebiete umfassen entsprechende Arbeiten zur Aussagenlogik und Automatentheorie, der Prädikatenlogik, automatischen Induktionsbeweisen, Logiken höherer Ordnung sowie zu temporalen Logiken. Es werden Tautologie-Checker, der Boyer-Moore-Beweiser, HOL und Termersetzungsbasierte Methoden untersucht. Das Ziel des Seminars ist, die Stärken und Schwächen der einzelnen Systeme zu erarbeiten und gegenüberzustellen.

Literatur:

1. A. Gupta. Formal Hardware Verfication: A Survey. Formal Methods in System Design, 1992.

Weitere Literatur wird in der Vorbesprechung bekannt gegeben.

Zurück zur Übersicht